i:Id, ds:x:Id fp Type, da:k:Knd fp Type, A:ecl(ds;da), k:Knd, l:IdLnk, tg:Id, n:,
f:(State(ds)Valtype(da;k)da(rcv(l,tg))?Void), es:ES.
source(l) = i
 (@i[[A;k sends on l with tag tg [s,v.f(s,v)], at marker n]]
 (
 ((es-decls(es;i;ds;da)
 (( with decls ds 
 (( with decls da
 (( sends on l from e 
 (( include if kind(e) = k  action[[A n]][es-init(es;e);e] [<tg,f((state when e),val(e))>]
 (( include else nil fi 
 (( and only these for tags in [tg])) 

latex

Definitions	x:A. B(x), P  Q, P  Q, x(s1,s2), P & Q, P  Q, t  T, Prop, x,y. t(x;y), x. t(x), SQType(T), {T}, Top, @i[[x;snd]], k sends on l with tag tg [s,v.f(s;v)], at marker n, x(s)
Lemmas	ecl-mng-sends wf, msg-spec1 wf, ma-valtype wf, Id wf, lsrc wf, event system wf, decl-state wf, fpf-cap wf, Knd wf, Kind-deq wf, rcv wf, nat wf, IdLnk wf, ecl wf, fpf wf, Id sq, ecl-tags-spec1